COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	$$M0BDB30$.
C00011 ENDMK
C⊗;
$$M0BDB30;$.
$F0FOL Project 1 Feb 1974
TASK DESCRIPTION #1

DECISION PROCEDURE FOR THE ALGEBRA OF SETS AND SOME OTHER ALGEBRAIC SYSTEMS


$J	This  is  the first  of  a series  of  memos  describing some
improvements that need to be made  to FOL.  The purpose of the  memos
is to aid in  dividing up the work and to  make possible consensus on
what the improvements should be.

	The algebra of sets is a part of set theory not involving the
ε  relation. In  its  simplest  form  it involves  the  operations  ∪
(union), ∩  (intersection) and ~  (complementation with respect  to a
universal set USET).  The following are universally valid formulas:$.

	1. x ∪ (y ∪ z) = (x ∪ y) ∪ z associativity
	2. x ∩ (y ∩ z) = (x ∩ y) ∩ z
	3. x ∩ (y ∩ z) = (x ∩ y) ∪ (x ∩ z)
	4. x ∪ (y ∩ z) = (x ∪ y) ∩ (x ∪ z)
	5. x ∩ x = x
	6. x ∪ x = x
	7. ~(x ∪ y) = ~x ∩ ~y
	8. ~(x ∩ y = ~x ∪ ~y
	9. ~~x = x
	10. ~NLSET = USET
	11. ~USET = NLSET
	12. x ∪ NLSET = x
	13. x ∩ NLSET = NLSET
	14. x ∪ USET = USET
	15. x ∩ USET = x.

$J	These  laws  are  identical  to  laws  of  the  propositional
calculus with  ∨, ∧,  ¬, ≡,  false, and  true replacing ∪,  ∩, ~,  =,
NLSET, and USET respectively.

	Therefore, the program taut, already part of FOL, can be used
to decide  whether a  formula involving  these  operators follows  by
Boolean algebra  from a collection  of other  formulas.  All  that is
required  is  a program  that  translates the  Boolean  formulas into
logical  formulas and  uses  taut.    (Indeed, if  only  the  Boolean
operations were  to be used, one  would not want both  the Boolean an
propositional operators).

	There is one minor embarassment that is easily fixed.   While
the universal set USET leads to no trouble  in Boolean algebra and is
a  convenient  fiction,  in conjunction  with  the  other axioms  and
operations of  ZF, it  leads to  a contradiction.    Therefore it  is
necesary  to  replace  the  complementation  operation  ~  by  a  set
difference operation  and get rid of USET.  We can write setdiff(x,y)
or x\y (or even x - y if the sort features of FOL can be straightened
out to permit  using - for both sets and numbers).   We can still use
taut; we have only to translate setdiff(x,y) into x∧¬y.

	Therefore, we can have a rule  booltaut in FOL that will  let
us  assert  any  formula that  follows  by  Boolean  algebra  from  a
collection  of lines of the  proof or axioms or  stored theorems.  As
with propositional formulas, the  Boolean formulas can involve  other
than Boolean  operators, expressions involving these  other operators
being treated as atoms in the Boolean algebra.

	However, booltaut needs some syntactic sugar, namely

	1. Since ∪ and ∩ are associative, we need to be able to write
x ∪ y ∪ z, etc.

	2. Instead of  writing only equalities,  we want also to  use
the inclusion symbol ⊂. This is handled by translating x ⊂ y into x ⊃
y.

	3. We  need the  operator {x,y,...,z}  for explicitly  listed
sets. This can  be done by  regarding {x,y,...,z} as  an abbreviation
for unitset(x) ∪ unitset(y) ∪ ... unitset(z).

	4.  Expressions of  the  form x  ε A  can  be allowed  in the
formulas by transforming them into unitset(x) ⊂ A.

	5. Conjunctions of Boolean algebra formulas can be allowed in
premisses and  conclusions since  the program can  replace them  by a
number of separate formulas.

	Besides  these features  which can be  added without changing
the reliance  on taut, there  are some  possible extensions that  may
require  additional mathematics  to determine  whether the  domain is
still decidable and  whether decision procedures  are feasible.  Here
are some possibilities:

	1.  Can we  allow  other  propositional combinations  of  the
Boolean  formulas in the  premisses and  conclusions?  This  seems to
require at least the elementary theory of equality.

	2. Can we include the Cartesian product in the algebra?$.


OTHER ALGEBRAIC SYSTEMS

$J	1. Associativity.  Certain operators are associative,  and if
we can't  write them in  binary form, proofs of  certain equivalences
can  be quite tedious. It would be  best if having proved an operator
associative, we could write it without grouping the terms in twos and
make  all deductions  depending solely  on its  associativity  in one
step.

	2. Commutativity.  The  previous remark applies here  without
change.

	3. Distributive pairs of operators.  The  case where there is
a  commutative operator  written  additively and  another associative
operator which obeys distributive laws  with respect to the first  is
quite common.  Sometimes  the multiplicative operator is distributive
also.   In  these cases  formal multiplication and  exponentiation by
integers also occur.  There are a number of cases,  but in each case,
informal  proofs  make heavy  use  of  what  are apparently  decision
procedures.$.


FINAL REMARK

$J	The possibility  that  there  are  a  large  number  of  such
elementary proof search procedures that will have  to be added to FOL
to  make  proofs as  short  as informal  ones  is  somewhat daunting.
Perhaps there is  a general way  of adding  the possibility of  proof
search procedures to FOL simply by reading in files.$.